(* Preliminaries concerning the involved data types and auxiliary functions *) theory Prelim imports "Fresh_Identifiers.Fresh_String" "Bounded_Deducibility_Security.Trivia" begin subsection â¹The basic types⺠(* This version of string is needed for code generation: *) type_synonym string = String.literal definition "emptyStr = STR ''''" type_synonym phase = nat (* Conference phases: no phase, setup, submission, bidding, reviewing, discussion, notification, closed *) abbreviation "noPH â¡ (0::nat)" abbreviation "setPH â¡ Suc noPH" abbreviation "subPH â¡ Suc setPH" abbreviation "bidPH â¡ Suc subPH" abbreviation "revPH â¡ Suc bidPH" abbreviation "disPH â¡ Suc revPH" abbreviation "notifPH â¡ Suc disPH" abbreviation "closedPH â¡ Suc notifPH" fun SucPH where "SucPH ph = (if ph = closedPH then closedPH else Suc ph)" (* The users of the system: *) datatype user = User string string string fun nameUser where "nameUser (User name info email) = name" fun infoUser where "infoUser (User name info email) = info" fun emailUser where "emailUser (User name info email) = email" definition "emptyUser â¡ User emptyStr emptyStr emptyStr" typedecl raw_data code_printing type_constructor raw_data â (Scala) "java.io.File" (* paper content: *) datatype pcontent = NoPContent | PContent raw_data